T:Type, L:T List, P1, P2, Q:(||L||Prop), R:(||L||||L||Prop).
(i:||L||. P1(i)  P2(i))  causal_order(L;R;P1;Q)  causal_order(L;R;P2;Q) 

latex

Definitions	t  T, P  Q, x:A. B(x), ||as||, False, A, AB, P & Q, i  j < k, {i..j}, Prop, x:A. B(x), causal_order(L;R;P;Q)
Lemmas	int seg wf, length wf1, le wf